The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(X) → n__terms(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(X)
activate(n__first(X1, X2)) → first(X1, X2)
activate(X) → X

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of add: sqr, add, dbl
The following defined symbols can occur below the 1th argument of add: dbl

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
half(dbl(X)) → X

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

half(s(0)) → 0
dbl(0) → 0
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
half(0) → 0
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
first(0, X) → nil
dbl(s(X)) → s(s(dbl(X)))
activate(X) → X
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__terms(X)) → terms(X)
sqr(0) → 0
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(X1, X2) → n__first(X1, X2)
sqr(s(X)) → s(add(sqr(X), dbl(X)))
half(s(s(X))) → s(half(X))

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

half(s(0)) → 0 [1]
dbl(0) → 0 [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
half(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
first(0, X) → nil [1]
dbl(s(X)) → s(s(dbl(X))) [1]
activate(X) → X [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(X1, X2) → n__first(X1, X2) [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
half(s(s(X))) → s(half(X)) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

half(s(0)) → 0 [1]
dbl(0) → 0 [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
half(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
first(0, X) → nil [1]
dbl(s(X)) → s(s(dbl(X))) [1]
activate(X) → X [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(X1, X2) → n__first(X1, X2) [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
half(s(s(X))) → s(half(X)) [1]

The TRS has the following type information:

half :: 0:s → 0:s s :: 0:s → 0:s 0 :: 0:s dbl :: 0:s → 0:s first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil cons :: recip → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil n__first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil activate :: cons:n__first:n__terms:nil → cons:n__first:n__terms:nil terms :: 0:s → cons:n__first:n__terms:nil n__terms :: 0:s → cons:n__first:n__terms:nil recip :: 0:s → recip sqr :: 0:s → 0:s nil :: cons:n__first:n__terms:nil add :: 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

half
first
terms
activate

(c) The following functions are completely defined:

sqr
dbl
add

Due to the following rules being added:
none

And the following fresh constants:

const

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: half(s(0)) → 0 [1] dbl(0) → 0 [1] first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1] half(0) → 0 [1] terms(X) → n__terms(X) [1] terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1] first(0, X) → nil [1] dbl(s(X)) → s(s(dbl(X))) [1] activate(X) → X [1] activate(n__first(X1, X2)) → first(X1, X2) [1] activate(n__terms(X)) → terms(X) [1] sqr(0) → 0 [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(X1, X2) → n__first(X1, X2) [1] sqr(s(X)) → s(add(sqr(X), dbl(X))) [1] half(s(s(X))) → s(half(X)) [1] The TRS has the following type information: half :: 0:s → 0:s s :: 0:s → 0:s 0 :: 0:s dbl :: 0:s → 0:s first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil cons :: recip → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil n__first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil activate :: cons:n__first:n__terms:nil → cons:n__first:n__terms:nil terms :: 0:s → cons:n__first:n__terms:nil n__terms :: 0:s → cons:n__first:n__terms:nil recip :: 0:s → recip sqr :: 0:s → 0:s nil :: cons:n__first:n__terms:nil add :: 0:s → 0:s → 0:s const :: recip Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: half(s(0)) → 0 [1] dbl(0) → 0 [1] first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1] half(0) → 0 [1] terms(X) → n__terms(X) [1] terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1] first(0, X) → nil [1] dbl(s(X)) → s(s(dbl(X))) [1] activate(X) → X [1] activate(n__first(X1, X2)) → first(X1, X2) [1] activate(n__terms(X)) → terms(X) [1] sqr(0) → 0 [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(X1, X2) → n__first(X1, X2) [1] sqr(s(0)) → s(add(0, 0)) [3] sqr(s(s(X'))) → s(add(s(add(sqr(X'), dbl(X'))), s(s(dbl(X'))))) [3] half(s(s(X))) → s(half(X)) [1] The TRS has the following type information: half :: 0:s → 0:s s :: 0:s → 0:s 0 :: 0:s dbl :: 0:s → 0:s first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil cons :: recip → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil n__first :: 0:s → cons:n__first:n__terms:nil → cons:n__first:n__terms:nil activate :: cons:n__first:n__terms:nil → cons:n__first:n__terms:nil terms :: 0:s → cons:n__first:n__terms:nil n__terms :: 0:s → cons:n__first:n__terms:nil recip :: 0:s → recip sqr :: 0:s → 0:s nil :: cons:n__first:n__terms:nil add :: 0:s → 0:s → 0:s const :: recip Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 0
const => 0

(12) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ terms(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(X)) :|: z = 1 + X, X >= 0
first(z, z') -{ 1 }→ 0 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
first(z, z') -{ 1 }→ 1 + Y + (1 + X + activate(Z)) :|: Z >= 0, z = 1 + X, Y >= 0, X >= 0, z' = 1 + Y + Z
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(X) :|: z = 1 + (1 + X), X >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(X'), dbl(X')), 1 + (1 + dbl(X'))) :|: X' >= 0, z = 1 + (1 + X')
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0

(13) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

(15) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ dbl } { add } { half } { sqr } { terms } { first, activate }

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {half}, {sqr}, {terms}, {first,activate}

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: ?, size: O(n1) [2·z]

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(21) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: ?, size: O(n1) [z + z']

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(27) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: ?, size: O(n1) [z]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(33) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z + 4·z²

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: ?, size: O(n2) [1 + 4·z + 4·z2]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 22·z + 8·z³

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s'), 1 + (1 + s'')) :|: s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(39) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 6 + 6·z + 4·z²

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: ?, size: O(n2) [6 + 6·z + 4·z2]

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 7 + 22·z + 8·z³

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2]

(45) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s8 :|: s8 >= 0, s8 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

Computed SIZE bound using CoFloCo for: activate
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s8 :|: s8 >= 0, s8 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2] first: runtime: ?, size: INF activate: runtime: ?, size: INF

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 3 + 48·z' + 8·z'³

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 94·z + 16·z³

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s8 :|: s8 >= 0, s8 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s) :|: s >= 0, s <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s5 + s6 + 120·z + -48·z² + 8·z³ }→ 1 + s7 :|: s5 >= 0, s5 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s6 >= 0, s6 <= 1 * s5 + 1 * s', s7 >= 0, s7 <= 1 * (1 + s6) + 1 * (1 + (1 + s'')), s' >= 0, s' <= 2 * (z - 2), s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s4) + (1 + (1 + z)) :|: s4 >= 0, s4 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2] first: runtime: O(n3) [3 + 48·z' + 8·z'3], size: INF activate: runtime: O(n3) [5 + 94·z + 16·z3], size: INF

(51) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(52) BOUNDS(1, n^3)